2024-11-09 Functional Programming in Lean

7.1の演習から

$ lean --run ./Ex2.lean -- --all

code:lean.hs

def ReaderT (ρ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=

ρ → m α

code:lean.hs

class MonadReader (ρ : outParam (Type u)) (m : Type u → Type v) : Type (max (u + 1) v) where

read : m ρ

read := fun env => pure env

export MonadReader (read)

noneまたはsomeの帰納型

code:lean.hs

-- inductive Option (α : Type u) where

-- /-- No value. -/

-- | none : Option α

-- | some (val : α) : Option α

def OptionT (m : Type u → Type v) (α : Type u) : Type v :=

-- αの型をOptionで包んでmで返す

m (Option α)

def getSomeInput : OptionT IO String := do

let input ← (← IO.getStdin).getLine

let trimmed := input.trim

if trimmed == "" then

failure

else pure trimmed

structure UserInfo where

name : String

favoriteBeetle : String

def getUserInfo : OptionT IO UserInfo := do

IO.println "What is your name?"

let name ← getSomeInput

IO.println "What is your favorite species of beetle?"

let beetle ← getSomeInput

pure ⟨name, beetle⟩

def interact : IO Unit := do

match ← getUserInfo with

| none => IO.eprintln "Missing info"

| some ⟨name, beetle⟩ => IO.println s!"Hello {name}, whose favorite beetle is {beetle}."